The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

0 CpxRelTRS
↳1 DecreasingLoopProof (⇔, 1780 ms)
↳2 BOUNDS(n^1, INF)
↳3 RenamingProof (⇔, 0 ms)
↳4 CpxRelTRS
    ↳5 SlicingProof (LOWER BOUND(ID), 0 ms)
    ↳6 CpxRelTRS
    ↳7 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 typed CpxTrs
    ↳9 OrderProof (LOWER BOUND(ID), 0 ms)
    ↳10 typed CpxTrs
    ↳11 RewriteLemmaProof (LOWER BOUND(ID), 296 ms)
    ↳12 BEST
        ↳13 typed CpxTrs
            ↳14 RewriteLemmaProof (LOWER BOUND(ID), 854 ms)
            ↳15 BEST
                ↳16 typed CpxTrs
                    ↳17 RewriteLemmaProof (LOWER BOUND(ID), 216 ms)
                    ↳18 BEST
                        ↳19 typed CpxTrs
                            ↳20 RewriteLemmaProof (LOWER BOUND(ID), 1809 ms)
                            ↳21 BEST
                                ↳22 typed CpxTrs
                                    ↳23 LowerBoundsProof (⇔, 0 ms)
                                    ↳24 BOUNDS(n^1, INF)
                                ↳25 typed CpxTrs
                                    ↳26 LowerBoundsProof (⇔, 0 ms)
                                    ↳27 BOUNDS(n^1, INF)
                        ↳28 typed CpxTrs
                            ↳29 LowerBoundsProof (⇔, 0 ms)
                            ↳30 BOUNDS(n^1, INF)
                ↳31 typed CpxTrs
                    ↳32 LowerBoundsProof (⇔, 0 ms)
                    ↳33 BOUNDS(n^1, INF)
        ↳34 typed CpxTrs
            ↳35 LowerBoundsProof (⇔, 0 ms)
            ↳36 BOUNDS(1, INF)

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), x, a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
red[Let][Let](e, Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](e, App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](e, V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](App(e1, e2), f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, x, a, e) → e
subst[Ite](True, x, a, e) → a

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
subst(x, a, App(e1, e2)) →+ mkapp(subst(x, a, e1), subst(x, a, e2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [e1 / App(e1, e2)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), x, a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](e, Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](e, App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](e, V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](App(e1, e2), f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, x, a, e) → e
subst[Ite](True, x, a, e) → a

Rewrite Strategy: INNERMOST

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
subst[Ite]/1
red[Let][Let]/0

(6) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

(9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
subst, eqTerm, red, !EQ

They will be analysed ascendingly in the following order:
eqTerm < subst
subst < red
!EQ < eqTerm

(10) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

The following defined symbols remain to be analysed:
!EQ, subst, eqTerm, red

They will be analysed ascendingly in the following order:
eqTerm < subst
subst < red
!EQ < eqTerm

(11) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)

Induction Base:
!EQ(gen_S:0'5_0(0), gen_S:0'5_0(+(1, 0))) →RΩ(0)
False

Induction Step:
!EQ(gen_S:0'5_0(+(n7_0, 1)), gen_S:0'5_0(+(1, +(n7_0, 1)))) →RΩ(0)
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) →IH
False

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).

(12) Complex Obligation (BEST)

(13) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)

Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

The following defined symbols remain to be analysed:
eqTerm, subst, red

They will be analysed ascendingly in the following order:
eqTerm < subst
subst < red

(14) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)

Induction Base:
eqTerm(gen_App:Lam:V4_0(+(1, 0)), gen_App:Lam:V4_0(0)) →RΩ(1)
False

Induction Step:
eqTerm(gen_App:Lam:V4_0(+(1, +(n510_0, 1))), gen_App:Lam:V4_0(+(n510_0, 1))) →RΩ(1)
and(eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)), eqTerm(V(0'), V(0'))) →IH
and(False, eqTerm(V(0'), V(0'))) →RΩ(1)
and(False, !EQ(0', 0')) →RΩ(0)
and(False, True) →RΩ(0)
False

We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

(15) Complex Obligation (BEST)

(16) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)

Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

The following defined symbols remain to be analysed:
subst, red

They will be analysed ascendingly in the following order:
subst < red

(17) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)) → gen_App:Lam:V4_0(n369658_0), rt ∈ Ω(1 + n3696580)

Induction Base:
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(0)) →RΩ(1)
subst[Ite](eqTerm(gen_App:Lam:V4_0(1), V(0')), gen_App:Lam:V4_0(b), V(0')) →LΩ(1)
subst[Ite](False, gen_App:Lam:V4_0(b), V(0')) →RΩ(0)
V(0')

Induction Step:
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(+(n369658_0, 1))) →RΩ(1)
mkapp(subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)), subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) →IH
mkapp(gen_App:Lam:V4_0(c369659_0), subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) →RΩ(1)
mkapp(gen_App:Lam:V4_0(n369658_0), subst[Ite](eqTerm(gen_App:Lam:V4_0(1), V(0')), gen_App:Lam:V4_0(b), V(0'))) →LΩ(1)
mkapp(gen_App:Lam:V4_0(n369658_0), subst[Ite](False, gen_App:Lam:V4_0(b), V(0'))) →RΩ(0)
mkapp(gen_App:Lam:V4_0(n369658_0), V(0')) →RΩ(1)
App(gen_App:Lam:V4_0(n369658_0), V(0'))

We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

(18) Complex Obligation (BEST)

(19) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)) → gen_App:Lam:V4_0(n369658_0), rt ∈ Ω(1 + n3696580)

Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

The following defined symbols remain to be analysed:
red

(20) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
red(gen_App:Lam:V4_0(n374659_0)) → *6_0, rt ∈ Ω(n3746590)

Induction Base:
red(gen_App:Lam:V4_0(0))

Induction Step:
red(gen_App:Lam:V4_0(+(n374659_0, 1))) →RΩ(1)
red[Let](App(gen_App:Lam:V4_0(n374659_0), V(0')), red(gen_App:Lam:V4_0(n374659_0))) →IH
red[Let](App(gen_App:Lam:V4_0(n374659_0), V(0')), *6_0)

We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

(21) Complex Obligation (BEST)

(22) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)) → gen_App:Lam:V4_0(n369658_0), rt ∈ Ω(1 + n3696580)
red(gen_App:Lam:V4_0(n374659_0)) → *6_0, rt ∈ Ω(n3746590)

Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

No more defined symbols left to analyse.

(23) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)

(24) BOUNDS(n^1, INF)

(25) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)) → gen_App:Lam:V4_0(n369658_0), rt ∈ Ω(1 + n3696580)
red(gen_App:Lam:V4_0(n374659_0)) → *6_0, rt ∈ Ω(n3746590)

Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

No more defined symbols left to analyse.

(26) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)

(27) BOUNDS(n^1, INF)

(28) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)
subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369658_0)) → gen_App:Lam:V4_0(n369658_0), rt ∈ Ω(1 + n3696580)

Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

No more defined symbols left to analyse.

(29) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)

(30) BOUNDS(n^1, INF)

(31) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)

Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

No more defined symbols left to analyse.

(32) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
eqTerm(gen_App:Lam:V4_0(+(1, n510_0)), gen_App:Lam:V4_0(n510_0)) → False, rt ∈ Ω(1 + n5100)

(33) BOUNDS(n^1, INF)

(34) Obligation:

Innermost TRS:
Rules:
subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2))
subst(x, a, Lam(var, exp)) → subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp))
red(App(e1, e2)) → red[Let](App(e1, e2), red(e1))
red(Lam(int, term)) → Lam(int, term)
subst(x, a, V(int)) → subst[Ite](eqTerm(x, V(int)), a, V(int))
red(V(int)) → V(int)
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22))
eqTerm(App(t11, t12), Lam(i2, l2)) → False
eqTerm(App(t11, t12), V(v2)) → False
eqTerm(Lam(i1, l1), App(t21, t22)) → False
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2))
eqTerm(Lam(i1, l1), V(v2)) → False
eqTerm(V(v1), App(t21, t22)) → False
eqTerm(V(v1), Lam(i2, l2)) → False
eqTerm(V(v1), V(v2)) → !EQ(v1, v2)
mklam(V(name), e) → Lam(name, e)
lamvar(Lam(var, exp)) → V(var)
lambody(Lam(var, exp)) → exp
isvar(App(t1, t2)) → False
isvar(Lam(int, term)) → False
isvar(V(int)) → True
islam(App(t1, t2)) → False
islam(Lam(int, term)) → True
islam(V(int)) → False
appe2(App(e1, e2)) → e2
appe1(App(e1, e2)) → e1
mkapp(e1, e2) → App(e1, e2)
lambdaint(e) → red(e)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
red[Let][Let](Lam(var, exp), a) → red(subst(V(var), a, exp))
subst[True][Ite](False, x, a, Lam(var, exp)) → mklam(V(var), subst(x, a, exp))
red[Let][Let](App(t1, t2), e2) → App(App(t1, t2), e2)
red[Let][Let](V(int), e2) → App(V(int), e2)
red[Let](App(e1, e2), f) → red[Let][Let](f, red(e2))
subst[True][Ite](True, x, a, e) → e
subst[Ite](False, a, e) → e
subst[Ite](True, a, e) → a

Types:
subst :: App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
App :: App:Lam:V → App:Lam:V → App:Lam:V
mkapp :: App:Lam:V → App:Lam:V → App:Lam:V
Lam :: S:0' → App:Lam:V → App:Lam:V
subst[True][Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V → App:Lam:V
eqTerm :: App:Lam:V → App:Lam:V → False:True
V :: S:0' → App:Lam:V
red :: App:Lam:V → App:Lam:V
red[Let] :: App:Lam:V → App:Lam:V → App:Lam:V
subst[Ite] :: False:True → App:Lam:V → App:Lam:V → App:Lam:V
and :: False:True → False:True → False:True
False :: False:True
!EQ :: S:0' → S:0' → False:True
mklam :: App:Lam:V → App:Lam:V → App:Lam:V
lamvar :: App:Lam:V → App:Lam:V
lambody :: App:Lam:V → App:Lam:V
isvar :: App:Lam:V → False:True
True :: False:True
islam :: App:Lam:V → False:True
appe2 :: App:Lam:V → App:Lam:V
appe1 :: App:Lam:V → App:Lam:V
lambdaint :: App:Lam:V → App:Lam:V
S :: S:0' → S:0'
0' :: S:0'
red[Let][Let] :: App:Lam:V → App:Lam:V → App:Lam:V
hole_App:Lam:V1_0 :: App:Lam:V
hole_S:0'2_0 :: S:0'
hole_False:True3_0 :: False:True
gen_App:Lam:V4_0 :: Nat → App:Lam:V
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)

Generator Equations:
gen_App:Lam:V4_0(0) ⇔ V(0')
gen_App:Lam:V4_0(+(x, 1)) ⇔ App(gen_App:Lam:V4_0(x), V(0'))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

No more defined symbols left to analyse.

(35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
!EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) → False, rt ∈ Ω(0)

(36) BOUNDS(1, INF)